(set-option :produce-models true)
(set-logic QF_AUFBV)
(declare-const bv (_ BitVec 32))
(define-fun A () (Array (_ BitVec 4) (_ BitVec 8)) ((as const (Array (_ BitVec 4) (_ BitVec 8))) (_ bv0 8)))
(define-fun f ((x (_ BitVec 8))) (_ BitVec 8) (bvadd x (_ bv1 8)))
(check-sat)
(get-value (A))
(get-value ((store A (_ bv4 4) (_ bv1 8))))
(get-value ((_ bv10 8)))
(get-value (bv (bvnot bv)))
(get-value (f))
(exit)
